Nuprl Lemma : fpf_wf
0,22
postcript
pdf
A
:Type,
B
:(
A
Type).
a
:
A
fp
B
(
a
)
Type
latex
Definitions
a
:
A
fp
B
(
a
)
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
t
T
Lemmas
l
member
wf
origin
A:Type, B:(A
Type). a:A fp B(a) 
Type A:Type, B:(AType). a:A fp B(a) Type B(a) l)x:A. B(x) T